<html>
<head><meta charset="utf-8"><title>Symbolic execution of MIR · t-compiler/const-eval · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/index.html">t-compiler/const-eval</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html">Symbolic execution of MIR</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="162094330"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/162094330" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#162094330">(Mar 30 2019 at 00:09)</a>:</h4>
<p>Hello everyone, I'm doing some work related to const generics which is writing an small symbolic interpreter for MIR as a part of my masters thesis. Right now it can only execute a reduced set of MIR expressions but I believe it could be explored further. </p>
<p>I'd like to know if there is some way of taking Rust code, compile it into MIR and then use my code to execute and manipulate the resulting MIR code, I assume this is possible given that miri is a separated project</p>



<a name="162132449"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/162132449" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> oli <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#162132449">(Mar 30 2019 at 18:06)</a>:</h4>
<p>You'll have to create your own driver (see <code>src/bin/miri.rs</code> in miri or <code>src/bin/driver.rs</code> in clippy). You can fetch the main function's MIR like miri does it and then process the resulting MIR as your see fit</p>



<a name="162138628"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/162138628" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#162138628">(Mar 30 2019 at 20:57)</a>:</h4>
<p>Thank you! I'm just checking  <code>src/bin/miri.rs</code>. I guess that in <a href="https://github.com/rust-lang/miri/blob/master/src/bin/miri.rs#L44" target="_blank" title="https://github.com/rust-lang/miri/blob/master/src/bin/miri.rs#L44">https://github.com/rust-lang/miri/blob/master/src/bin/miri.rs#L44</a> miri is fetching the id of the main function and then <code>miri::eval_main</code> will take the mir of the main function from the context using <code>entry_def_id</code>. Am i correct?</p>



<a name="162179864"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/162179864" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> oli <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#162179864">(Mar 31 2019 at 15:38)</a>:</h4>
<p>yes</p>



<a name="162363534"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/162363534" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#162363534">(Apr 02 2019 at 18:54)</a>:</h4>
<p>Thank you for your help! I've been able to do a lot since friday. Currently I can evaluate recursive functions without side effects and I hope to do a lot of improvements this week</p>



<a name="162363554"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/162363554" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#162363554">(Apr 02 2019 at 18:55)</a>:</h4>
<p>If anyone wants to see the code: <a href="https://github.com/christianpoveda/sire" target="_blank" title="https://github.com/christianpoveda/sire">https://github.com/christianpoveda/sire</a></p>



<a name="162716955"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/162716955" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#162716955">(Apr 06 2019 at 19:39)</a>:</h4>
<p>Currently my project is able to evaluate recursive functions with conditionals by creating an interpreter for each branch and leaving stated the recursive call. However, functions with loops cannot be evaluated given that blocks don't exist in my representation. It would make sense to try to separate the blocks in a loop into an auxiliary function? For example, if I have the function</p>
<div class="codehilite"><pre><span></span><span class="k">fn</span> <span class="nf">foo</span><span class="p">(</span><span class="n">x</span>: <span class="kt">u32</span><span class="p">)</span><span class="w"> </span>-&gt; <span class="kt">u32</span> <span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="kd">let</span><span class="w"> </span><span class="k">mut</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="mi">0</span><span class="p">;</span><span class="w"></span>
<span class="w">    </span><span class="kd">let</span><span class="w"> </span><span class="k">mut</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="mi">0</span><span class="p">;</span><span class="w"></span>
<span class="w">    </span><span class="k">while</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">&lt;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">        </span><span class="n">r</span><span class="w"> </span><span class="o">+=</span><span class="w"> </span><span class="n">i</span><span class="p">;</span><span class="w"></span>
<span class="w">        </span><span class="n">i</span><span class="w"> </span><span class="o">+=</span><span class="w"> </span><span class="mi">1</span><span class="p">;</span><span class="w"></span>
<span class="w">    </span><span class="p">}</span><span class="w"></span>
<span class="w">    </span><span class="n">r</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</pre></div>


<p>the MIR of <code>foo</code> contains the following transitions between basic blocks:<br>
- <code>bb0 -&gt;  bb1</code>.<br>
- <code>bb1 -&gt; bb2 or bb3</code><br>
- <code>bb3 -&gt; bb1</code></p>
<p>I was wondering if it is reasonable to move the blocks <code>bb1</code> and <code>bb3</code> to its own function to be able to write the MIR of <code>foo</code> as a recursive function. However, I'm worried about the differences when a panic happens for example. Also I'm not sure if the subset of MIR functions that are produced from valid Rust functions is restricted enough to be able to do this in all cases.</p>



<a name="162739926"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/162739926" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> oli <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#162739926">(Apr 07 2019 at 06:01)</a>:</h4>
<p>Can't you treat every BB as its own function in your evaluator? Instead of rewriting the MIR, just treat it as if that were the representation</p>



<a name="162765131"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/162765131" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#162765131">(Apr 07 2019 at 17:40)</a>:</h4>
<p>I could, but then some simple functions would have a really long representation</p>



<a name="162765145"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/162765145" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#162765145">(Apr 07 2019 at 17:40)</a>:</h4>
<p>I guess I could represent every block as a function and then check if I can inline it</p>



<a name="163748179"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163748179" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163748179">(Apr 19 2019 at 17:05)</a>:</h4>
<p>i was checking the mir generated for a function containing a <code>for</code> loop. I realized that even with level 3 optimizations the mir is really huge (or at least more than I expected after checking a similar function with a <code>while</code> loop. There are a couple terminators that i've never seen <code>falseEdges</code> and <code>falseUnwind</code>, what are those doing?</p>



<a name="163748262"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163748262" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163748262">(Apr 19 2019 at 17:06)</a>:</h4>
<p>that's NLL stuff, I think</p>



<a name="163748544"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163748544" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163748544">(Apr 19 2019 at 17:11)</a>:</h4>
<p>I was checking  the same function with the playground but I've realised that is smaller than mine. I guess release includes more compiler flags than just opt-level 3?</p>



<a name="163748628"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163748628" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163748628">(Apr 19 2019 at 17:12)</a>:</h4>
<p>release affects which MIR gets generated</p>



<a name="163748635"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163748635" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163748635">(Apr 19 2019 at 17:12)</a>:</h4>
<p>like, whether arithmetic is translated with or without overflow checks</p>



<a name="163748639"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163748639" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163748639">(Apr 19 2019 at 17:12)</a>:</h4>
<p>and debug assertions, obviously</p>



<a name="163748660"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163748660" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163748660">(Apr 19 2019 at 17:12)</a>:</h4>
<p>how can I reproduce the behaviour of the compiler under release using only rustc?</p>



<a name="163749582"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163749582" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163749582">(Apr 19 2019 at 17:26)</a>:</h4>
<p>release mode corresponds to the <code>-O</code> flag</p>



<a name="163749598"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163749598" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163749598">(Apr 19 2019 at 17:27)</a>:</h4>
<p>also see <code>rustc --help</code></p>



<a name="163749974"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163749974" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163749974">(Apr 19 2019 at 17:31)</a>:</h4>
<p><code>opt-level=2</code>?</p>



<a name="163750057"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163750057" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163750057">(Apr 19 2019 at 17:32)</a>:</h4>
<p>i see no discernible difference in the number of blocks</p>



<a name="163750071"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163750071" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163750071">(Apr 19 2019 at 17:32)</a>:</h4>
<p>there are around 30 and the playground version has 7</p>



<a name="163750639"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163750639" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Matthew Jasper <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163750639">(Apr 19 2019 at 17:41)</a>:</h4>
<blockquote>
<p>There are a couple terminators that i've never seen <code>falseEdges</code> and <code>falseUnwind</code>, what are those doing?</p>
</blockquote>
<p>These shouldn't exist in optimized MIR (after all passes have been performed).</p>



<a name="163752063"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163752063" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163752063">(Apr 19 2019 at 17:59)</a>:</h4>
<p><span class="user-mention" data-user-id="132916">@Christian Poveda</span> could you share the code you are using to test this?</p>



<a name="163752161"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163752161" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163752161">(Apr 19 2019 at 18:00)</a>:</h4>
<p><a href="https://play.integer32.com/?version=nightly&amp;mode=release&amp;edition=2018&amp;gist=7dfbc38e5d8b4e3e79cd37f8f0c5f6ed" target="_blank" title="https://play.integer32.com/?version=nightly&amp;mode=release&amp;edition=2018&amp;gist=7dfbc38e5d8b4e3e79cd37f8f0c5f6ed">https://play.integer32.com/?version=nightly&amp;mode=release&amp;edition=2018&amp;gist=7dfbc38e5d8b4e3e79cd37f8f0c5f6ed</a></p>



<a name="163752491"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163752491" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163752491">(Apr 19 2019 at 18:05)</a>:</h4>
<p>Is the MIR you're looking at locally produced by <code>rustc ... --emit mir</code> or is it (a dump of) the MIR that your custom driver gets?</p>



<a name="163753522"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163753522" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163753522">(Apr 19 2019 at 18:18)</a>:</h4>
<p><span class="user-mention" data-user-id="132916">@Christian Poveda</span> I can reproduce the playground output with just <code>rustc --emit mir -O file.rs</code></p>



<a name="163754462"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163754462" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163754462">(Apr 19 2019 at 18:30)</a>:</h4>
<p>Is the MIR I get when dumping the mir using the -Z flag</p>



<a name="163754468"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163754468" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163754468">(Apr 19 2019 at 18:30)</a>:</h4>
<p>Maybe im looking the wrong mir file?</p>



<a name="163754530"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163754530" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163754530">(Apr 19 2019 at 18:31)</a>:</h4>
<p>Oh the -Z flag might dump after every pass, in that case it would be very easy to look at a file that's wildly different from the final MIR that playground/<code>--emit mir</code> show</p>



<a name="163755574"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163755574" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163755574">(Apr 19 2019 at 18:45)</a>:</h4>
<p>I'm gonna check the mir i'd get from the custom driver</p>



<a name="163755750"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163755750" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163755750">(Apr 19 2019 at 18:47)</a>:</h4>
<p>Ok yes the driver gets a short mir also</p>



<a name="163755766"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163755766" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163755766">(Apr 19 2019 at 18:47)</a>:</h4>
<p>is it there any way to "emit" the .dot diagram for this?</p>



<a name="163755906"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163755906" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163755906">(Apr 19 2019 at 18:49)</a>:</h4>
<p>hm, it is still strange though that there are no dump files of <code>sum</code> from phase 3</p>



<a name="163755917"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163755917" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163755917">(Apr 19 2019 at 18:50)</a>:</h4>
<div class="codehilite"><pre><span></span>-rw-r--r-- 1 r r 10353 Apr 19 20:46 rustc.sum.001-000.SimplifyCfg-initial.after.mir
-rw-r--r-- 1 r r 11972 Apr 19 20:46 rustc.sum.001-000.SimplifyCfg-initial.before.mir
-rw-r--r-- 1 r r 10343 Apr 19 20:46 rustc.sum.001-001.TypeckMir.after.mir
-rw-r--r-- 1 r r 10344 Apr 19 20:46 rustc.sum.001-001.TypeckMir.before.mir
-rw-r--r-- 1 r r 10345 Apr 19 20:46 rustc.sum.001-002.SanityCheck.after.mir
-rw-r--r-- 1 r r 10346 Apr 19 20:46 rustc.sum.001-002.SanityCheck.before.mir
-rw-r--r-- 1 r r 10353 Apr 19 20:46 rustc.sum.001-003.UniformArrayMoveOut.after.mir
-rw-r--r-- 1 r r 10354 Apr 19 20:46 rustc.sum.001-003.UniformArrayMoveOut.before.mir
-rw-r--r-- 1 r r 10360 Apr 19 20:46 rustc.sum.002-000.QualifyAndPromoteConstants.after.mir
-rw-r--r-- 1 r r 10361 Apr 19 20:46 rustc.sum.002-000.QualifyAndPromoteConstants.before.mir
-rw-r--r-- 1 r r 10360 Apr 19 20:46 rustc.sum.002-001.SimplifyCfg-qualify-consts.after.mir
-rw-r--r-- 1 r r 10361 Apr 19 20:46 rustc.sum.002-001.SimplifyCfg-qualify-consts.before.mir
-rw-r--r-- 1 r r 11955 Apr 19 20:46 rustc.sum.-------.mir_map.0.mir
</pre></div>



<a name="163756058"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163756058" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163756058">(Apr 19 2019 at 18:51)</a>:</h4>
<p>ah... it's because the fn is never called so doesnt get dumped</p>



<a name="163756136"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163756136" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163756136">(Apr 19 2019 at 18:52)</a>:</h4>
<p><span class="user-mention" data-user-id="132916">@Christian Poveda</span> <code>mir_dump/rustc.sum.003-027.PreCodegen.after.mir</code> matches the MIR on playground</p>



<a name="163756140"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163756140" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163756140">(Apr 19 2019 at 18:52)</a>:</h4>
<p>generated by <code>rustc -Zdump-mir=all p.rs -O --emit mir</code></p>



<a name="163756185"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163756185" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163756185">(Apr 19 2019 at 18:53)</a>:</h4>
<p>also see <a href="https://github.com/rust-lang/rust/issues/43620" target="_blank" title="https://github.com/rust-lang/rust/issues/43620">https://github.com/rust-lang/rust/issues/43620</a></p>



<a name="163756288"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163756288" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163756288">(Apr 19 2019 at 18:54)</a>:</h4>
<p>oh ok, i guess that solves the problem</p>



<a name="163756780"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/163756780" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#163756780">(Apr 19 2019 at 19:00)</a>:</h4>
<p>well thank you both :) this has been really helpful</p>



<a name="164495076"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164495076" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164495076">(Apr 29 2019 at 22:42)</a>:</h4>
<p>It seems I'm misunderstanding the semantic of <code>StorageLive/Dead</code>, why the mir of the <code>is_odd</code> function does not have an <code>StorageLive(_4)</code> statement? <a href="https://play.integer32.com/?version=nightly&amp;mode=release&amp;edition=2018&amp;gist=756a4645cf1d86997a90708e1beb9966" target="_blank" title="https://play.integer32.com/?version=nightly&amp;mode=release&amp;edition=2018&amp;gist=756a4645cf1d86997a90708e1beb9966">https://play.integer32.com/?version=nightly&amp;mode=release&amp;edition=2018&amp;gist=756a4645cf1d86997a90708e1beb9966</a></p>



<a name="164510265"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164510265" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164510265">(Apr 30 2019 at 04:28)</a>:</h4>
<p>as a side question, why does 2 == 0 does not evaluate to false immediately?</p>



<a name="164527095"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164527095" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164527095">(Apr 30 2019 at 10:17)</a>:</h4>
<p>some variables are implicitly live and never have a <code>Storage</code> annotation. I don't know why.</p>



<a name="164537162"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164537162" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164537162">(Apr 30 2019 at 13:08)</a>:</h4>
<p>Uhhh i started a new thread by accident...</p>



<a name="164537313"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164537313" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164537313">(Apr 30 2019 at 13:10)</a>:</h4>
<p>I was thinking on just allocating space for every local at the same time when the function argument locals are allocated and freeing all the locals at the end of execution. Otherwise I'd have to check which locals lack of an <code>StorageLive</code> and <code>StorageDead</code> statement before even executing the function.</p>



<a name="164537553"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164537553" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> oli <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164537553">(Apr 30 2019 at 13:14)</a>:</h4>
<p>no that does not happen right now</p>



<a name="164537609"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164537609" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> oli <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164537609">(Apr 30 2019 at 13:15)</a>:</h4>
<p>yea, we do that check in clippy, but we optimized it out for some situations</p>



<a name="164537826"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164537826" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164537826">(Apr 30 2019 at 13:18)</a>:</h4>
<p>I guess for the moment is enough to reserve everyone at the same time and just ignore the <code>Storage</code> statements then, I'll let a comment on my code in case this becomes relevant after</p>



<a name="164537884"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164537884" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164537884">(Apr 30 2019 at 13:19)</a>:</h4>
<blockquote>
<p>It seems I'm misunderstanding the semantic of <code>StorageLive/Dead</code>, why the mir of the <code>is_odd</code> function does not have an <code>StorageLive(_4)</code> statement? <a href="https://play.integer32.com/?version=nightly&amp;mode=release&amp;edition=2018&amp;gist=756a4645cf1d86997a90708e1beb9966" target="_blank" title="https://play.integer32.com/?version=nightly&amp;mode=release&amp;edition=2018&amp;gist=756a4645cf1d86997a90708e1beb9966">https://play.integer32.com/?version=nightly&amp;mode=release&amp;edition=2018&amp;gist=756a4645cf1d86997a90708e1beb9966</a></p>
</blockquote>
<p>I have another question, why on that specific example <code>_4</code> is not resolved to false during compilation?</p>



<a name="164537888"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164537888" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> oli <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164537888">(Apr 30 2019 at 13:19)</a>:</h4>
<p>I think the only thing that can be problematic with the way you're addressing is that you may not notice if someone is accessing a dangling pointer, because your local still lives</p>



<a name="164538033"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164538033" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164538033">(Apr 30 2019 at 13:21)</a>:</h4>
<blockquote>
<p>I think the only thing that can be problematic with the way you're addressing is that you may not notice if someone is accessing a dangling pointer, because your local still lives</p>
</blockquote>
<p>Jmm... the other option is to still allocate and free using <code>StorageLive/Dead</code> and also at the beginning and end of execution and do double frees #YOLO</p>



<a name="164538141"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164538141" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> oli <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164538141">(Apr 30 2019 at 13:22)</a>:</h4>
<blockquote>
<blockquote>
<p>It seems I'm misunderstanding the semantic of <code>StorageLive/Dead</code>, why the mir of the <code>is_odd</code> function does not have an <code>StorageLive(_4)</code> statement? <a href="https://play.integer32.com/?version=nightly&amp;mode=release&amp;edition=2018&amp;gist=756a4645cf1d86997a90708e1beb9966" target="_blank" title="https://play.integer32.com/?version=nightly&amp;mode=release&amp;edition=2018&amp;gist=756a4645cf1d86997a90708e1beb9966">https://play.integer32.com/?version=nightly&amp;mode=release&amp;edition=2018&amp;gist=756a4645cf1d86997a90708e1beb9966</a></p>
</blockquote>
<p>I have another question, why on that specific example <code>_4</code> is not resolved to false during compilation?</p>
</blockquote>
<p>because <a href="#narrow/stream/189540-t-compiler.2Fwg-mir-opt/topic/Other.20available.20work.3F" title="#narrow/stream/189540-t-compiler.2Fwg-mir-opt/topic/Other.20available.20work.3F">https://rust-lang.zulipchat.com/#narrow/stream/189540-t-compiler.2Fwg-mir-opt/topic/Other.20available.20work.3F</a> is still a WIP (const propagation is not actually propagating yet)</p>



<a name="164538452"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164538452" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164538452">(Apr 30 2019 at 13:26)</a>:</h4>
<blockquote>
<blockquote>
<p>I think the only thing that can be problematic with the way you're addressing is that you may not notice if someone is accessing a dangling pointer, because your local still lives</p>
</blockquote>
<p>Jmm... the other option is to still allocate and free using <code>StorageLive/Dead</code> and also at the beginning and end of execution and do double frees #YOLO</p>
</blockquote>
<p>I thing I'm gonna do the Right Thing™ and check which locals lack of <code>StorageLive/Dead</code> statements. Is possible that one local has just one of those two?</p>



<a name="164538494"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164538494" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164538494">(Apr 30 2019 at 13:27)</a>:</h4>
<p>Meaning that they are allocated explicitly but freed at the end of the function, and viceversa?</p>



<a name="164538510"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164538510" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> oli <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164538510">(Apr 30 2019 at 13:27)</a>:</h4>
<p>I think that used to be a problem, not sure if it is anymore</p>



<a name="164538519"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164538519" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> oli <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164538519">(Apr 30 2019 at 13:27)</a>:</h4>
<p>miri just checks if either exist</p>



<a name="164539083"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164539083" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164539083">(Apr 30 2019 at 13:34)</a>:</h4>
<p>if a local has either, that's weird but shouldnt need a special case -- that local may not get used until a storagelive happened. (so if it has just a StorageDead, it may never be used at all.)</p>



<a name="164539237"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164539237" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164539237">(Apr 30 2019 at 13:37)</a>:</h4>
<p>I'll get hands on then</p>



<a name="164540201"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164540201" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164540201">(Apr 30 2019 at 13:50)</a>:</h4>
<p>Ok It worked!!!</p>



<a name="164540202"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164540202" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164540202">(Apr 30 2019 at 13:50)</a>:</h4>
<p>:D</p>



<a name="164543842"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164543842" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164543842">(Apr 30 2019 at 14:33)</a>:</h4>
<p>I'm going to check that the whole memory is empty after execution</p>



<a name="164543845"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146212-t-compiler/const-eval/topic/Symbolic%20execution%20of%20MIR/near/164543845" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Christian Poveda <a href="https://rust-lang.github.io/zulip_archive/stream/146212-t-compiler/const-eval/topic/Symbolic.20execution.20of.20MIR.html#164543845">(Apr 30 2019 at 14:33)</a>:</h4>
<p>just to be sure</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>